dcdr{-}to{-}bool($d$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$case $d$ of inl($x$) =$>$ inl $\cdot$  $\mid$ inr($x$) =$>$ inr $\cdot$